User blog:Syst3ms/Stellar OCF Formalization
This version is outdated and has been superseded by STON 2, described here. This is an attempt to formally define "Stellar OCF" (originally created by Ecl1psed). Some of the techniques used here to define the ordinal notation originate from Buchholz . I should clarify that "Stellar OCF" is the original name, and it's defined here as an ordinal notation, not an OCF. Hence, I will refer to it as STON from now on. Definition Set of formal strings \(T\) Definition of \(T\): *\(0 \in T\) *For \(a,b \in T\), \(a+b\in T\) *For \(a,b \in T\), \(\psi_a(b)\in T\) *For \(a \in T\), \(\psi^1(a)\in T\) Shorthands Base of the notation : Definition of \(PT\), the set of principal terms ''': *For \(a,b \in T\), \(\psi_a(b)\in PT\) *For \(a \in T\), \(\psi^1(a)\in PT\) Definition of \(ST\), the set of '''successor terms : *\(1\in ST\) *For \(a\in T\), \(a+1\in ST\) Definition of \(\text{pre}(s)\), the predecessor function : #If \(s\in \{0\}\cap PT\), \(\text{pre}(s)=0\) #Else if \(s=s_1+s_2\) with \(s_1\in PT,s_2\in T\) : ##If \(\text{pre}(s_2)=0\) then \(\text{pre}(s)=s_1\) ##Otherwise, \(\text{pre}(s)=s_1+\text{pre}(s_2)\) Definition of \(\text{cof}(s)\), the cofinality function: #If \(s=0\vee s=1\) then \(\text{cof}(s)=s\) #Else if \(s=\psi^1(a)\): ##If \(\text{cof}(a)\leq\omega\) then \(\text{cof}(s)=s\) ##Otherwise, \(\text{cof}(s)=\text{cof}(a)\) #Else if \(0<\text{lev}(s)\) then \(\text{cof}(s)=s\) #Else if \(s=s_1+s_2\) with \(s_1\in T,s_2\in PT\) then \(\text{cof}(s)=\text{cof}(s_2)\) #Else if \(s=\psi_a(b)\) : ##If \(\text{cof}(b)=1\vee a\leq\text{cof}(b)\) then \(\text{cof}(s)=\omega\) ##Otherwise, \(\text{cof}(s)=\text{cof}(b)\) Definition of \(\text{lev}(s)\), the level function : #If \(s=s_1+s_2\) with \(s_1\in T, s_2 \in PT\) then \(\text{lev}(s)=0\) #Else if \(s=\psi^1(a)\) : ##If \(\omega<\text{cof}(a)\) then \(\text{lev}(s)=0\) ##Else if \(a=0\) then \(\text{lev}(s)=1\) ##Else if \(a=a_1+a_2\) with \(a_1\in T,a_2 \in PT\) then \(\text{lev}(s)=\text{lev}(\psi^1(a_2))\) ##Else if \(a=\psi_b©\) and \(\text{lev}(b)=1\wedge \text{cof}(\psi_b©)\leq\omega\): ###If \(b\leq c\) then \(\text{lev}(s)=\nu_b©\), where \(\nu_p(s)\) is defined as such : ####\(\nu_p(0)=0\) ####Else if \(s=d+e\) with \(d\in PT,e\in T\) then \(\nu(s)=\nu_p(d)+\nu_p(e)\) ####Else if \(p\leq\text{cof}(s)\) then \(\nu_p(s)=\nu_p(S(\psi_p(s)))\) ####Otherwise, \(\nu_p(s)=s\) ###Else if \(\omega\leq c\) then \(\text{lev}(s)=c\) ###Else if \(c<\omega\) then \(\text{lev}(s)=c+1\) ###Otherwise, \(\text{lev}(s)=0\) ##Otherwise, \(\text{lev}(s)=0\) #Else if \(s=\psi_a(b)\) : ##If \(\text{lev}(a)\in ST\) then \(\text{lev}(s)=\text{pre}(\text{lev}(a))\) ##Else if \(b=b_1+b_2\) with \(b_1\notin ST\), \(b_2<\omega\) and \(\text{cof}(\text{lev}(a))=\omega\) then \(\text{lev}(s)=\text{lev}(a)b_2\) ##Otherwise, \(\text{lev}(s)=0\) Recursive comparison algorithm Comparison algorithm for \(sY ?" The problem is, we're dealing with infinite sets, so you could need TREE(3) steps to get a value of \(\alpha\) that works, if it exists at all... Thus, we need a process to get fundamental sequences that you could make a computer program that ends in finite time from. Well, we still can't use actual sets in our computations, because we might again run into questions such as "Is there a B such that A=psi(B) ?", and we have the same issue. Instead, we're going to use strings : plain, finite sequences of characters. But those strings can't be of any form, you can't just write "Canada" and expect it to give you an ordinal if your notation is meant to have functions and stuff. Therefore, we first need to define the entirety of strings that are of correct form (we say well-formed). This is what I do with \(T\). It starts by only having 0 inside of it, and then from this building block, you can build larger strings using \(\psi\), \(\psi^1\) and \(+\). We have well-formed strings now, but there are two major issues : *We have no way to compare them : they're just characters after all *Not all well-formed strings are valid ordinals : imagine something like \(\frac{1}{0}\). Sure it's something you can write given natural numbers and operators, but that doesn't mean it has a value. For both of them, we define some "helper" tools that will make the definitions much clearer and less cluttered. This is what \(PT,ST,\text{pre},\text{lev},\text{cof},G_\kappa\) do here. Their definition is specific to STON, and not important right now. All you need to know is that they will help us solve the two problems : #We solve the first one by simply defining a comparison algorithm between elements of \(T\). How you do that is not as simple as it sounds like, but it's usually manageable #We solve the second problem by introducing a subset of \(T\), \(OT\). This is the set of standard forms, which is supposed to forbid things that are well-formed, but illegal for the purposes of the notation, like \(\frac{1}{0}\). How it's restricted is also out of scope of this explanation. However, for the notation to actually describe ordinals, both of these must satisfy a few properties : *It is preferred for the comparison algorithm to be a total order, which just means that any two elements can be compared. More precisely, either one of \(s Category:Blog posts